FDL - Nuprl Lemma : member-insert-by

Nuprl Lemma : member-insert-by

T:Type, eq, r:(T

T

).
(

a, b:T. (

(eq(a,b)))

(a = b))

(

x:T, L:(T List), z:T. (z

insert-by(eq;r;x;L))

((z = x)

(z

L)))

Definitions s = t, t T, Type, , x:AB(x), b, <a, b>, , P Q, P Q, x:A B(x), P & Q, P Q, x:A. B(x), type List, (x l), left + right, P Q, A, Void, False, a < b, x:A. B(x), f(a), insert-by(eq;r;x;l), {T}, Dec(P), A B, b | a, a ~ b, a b, a <p b, a < b, A c B, x f y, xL. P(x), (xL.P(x)), , Atom, {i..j}, x,y:A//B(x;y), |p|, |g|, |r|, Unit, , , case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , [], [car / cdr], p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, , =, a < b, =, =, [d], b, p q, p q, p q, ff, tt

Lemmas member singleton, nil member, false wf, eqtt to assert, assert wf, not wf, bool wf, eqff to assert, assert of bnot, iff transitivity, iff functionality wrt iff, or functionality wrt iff, iff wf, rev implies wf, cons member, decidable or, l member wf